\begin{tabbing}
fischer{-}delay\=\{\=i:l,\+\+
\\[0ex]\$x:ut2,
\\[0ex]\$try:ut2,
\\[0ex]\$taken:ut2,
\\[0ex]\$contending:ut2,
\\[0ex]\$free:ut2,
\\[0ex]\$mine:ut2,
\\[0ex]\$wanted:ut2,
\\[0ex]\$z:ut2\}
\-\\[0ex](${\it es}$; ${\it del}$; $L$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](es{-}loc(${\it es}$; $e$) $\in$ $L$ $\in$ Id)
\\[0ex]$\Rightarrow$ \=(\=((es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$try:ut2\})\+\+
\\[0ex]$\vee$ es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$taken:ut2\}))
\\[0ex]$\Rightarrow$ \=(((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\} $\in$ Id)\+
\\[0ex]$\Rightarrow$ unchanged{-}for\=\{i:l\}\+
\\[0ex](Id; id{-}deq; ${\it es}$; mkid\{\$x:ut2\}; ${\it del}$; $e$))
\-\\[0ex]$\wedge$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\} $\in$ Id)\+
\\[0ex]$\Rightarrow$ unchanged{-}for\=\{i:l\}\+
\\[0ex](Id; id{-}deq; ${\it es}$; mkid\{\$x:ut2\}; (2 $\ast$ ${\it del}$); $e$))))
\-\-\-\-\\[0ex]$\wedge$ \=(es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$mine:ut2\})\+
\\[0ex]$\Rightarrow$ unchanged{-}for\=\{i:l\}\+
\\[0ex](Id; id{-}deq; ${\it es}$; mkid\{\$x:ut2\}; (2 $\ast$ ${\it del}$); $e$))
\-\-\\[0ex]$\wedge$ \=(((((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$contending:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ unchanged{-}for\=\{i:l\}\+
\\[0ex](Id; id{-}deq; ${\it es}$; mkid\{\$x:ut2\}; (2 $\ast$ ${\it del}$); $e$))
\-\\[0ex]$\vee$ \=((es{-}when(${\it es}$; mkid\{\$x:ut2\}; $e$) = mkid\{\$free:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ unchanged{-}for\=\{i:l\}\+
\\[0ex](Id; id{-}deq; ${\it es}$; mkid\{\$x:ut2\}; ${\it del}$; $e$)))
\-\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\} $\in$ Id)\+
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$ $\in$ IdLnk))))))
\-\-\-\\[0ex]$\Rightarrow$ es{-}change{-}to(${\it es}$;Id;mkid\{\$x:ut2\};$e$;mkid\{\$taken:ut2\}))
\-\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ \=((es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\} $\in$ Id)\+
\\[0ex]$\vee$ (es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\} $\in$ Id))
\-\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$ $\in$ IdLnk)))
\-\\[0ex]$\Rightarrow$ qless(es{-}time(${\it es}$; $e$); (es{-}time(${\it es}$; es{-}sender(${\it es}$; $e$)) + ${\it del}$))))
\-\-\-
\end{tabbing}